Section: New Results

Verification of spreadsheet programs by abstract interpretation

Participants : Tie Cheng, Xavier Rival.

Spreadsheet tools (Excel, Openoffice) come with powerful languages which can manipulate sheets in various ways. However, no type discipline is enforced, so that the programs may corrupt spreadsheet contents in many ways. We proposed an abstraction to describe sets of valid spreadsheet states, and designed a verifier for invariants expressed in this abstract domain. Our verifier assumes invariants are defined at the head of loops in the programs (as widening operators for the inference of loop invariants). This work was done as part of Tie Cheng Master internship.